Nuprl Definition : comp-atom-ap 11,40

comp-atom-ap(g; f; x; a)
== let f' = a.compose(g; f) in
== let f'let x' = a.x in
== let f'let x'let F = b,c. f'(b,x'(c)) in
== let f'let x'let Flet L = atoms-in(F) in
== let f'let x'let Flet Llet b = new-atom(cons(a; L)) in
== let f'let x'let Flet Llet bif eq_atom((F(b,a)); a)
== let f'let x'let Flet Llet bifthen inr (f'(b)) 
== let f'let x'let Flet Llet if eq_atom((F(a,b)); a)
== let f'let x'let Flet Llet ifthen inl (f.g(f(x'(b)))) 
== let f'let x'let Flet Llet else inr (x.hd(list-diff(atom-deq; monitor((f'(b,x))); cons(b; L)))) 
== let f'let x'let Flet Llet fi  
latex


Definitionscompose(f; g), let x = a in b(x), if b then t else f fi , eq_atom(x; y), inl x , inr x , x.A(x), hd(l), list-diff(eq; as; bs), atom-deq, f(a), cons(car; cdr)
FDL editor aliasescomp-atom-ap

origin